(* $Id: solver.mli 50 2007-10-01 14:42:23Z yann.regisgianas $ *)

(** This module provides a constraint solver based on unification
    under a mixed prefix. *)

open Position
type position = Position.t
open MultiEquation
open CoreAlgebra
open Constraint

(** The solver environment. *)
type 'syntax environment 

(** The constraint to solve. *)
type 'syntax tconstraint = 'syntax Constraint.tconstraint

(** A [solving_step] describes a elementary step of the solver. *)
type 'syntax solving_step = 
  | Init of 'syntax tconstraint
  | Solve of 'syntax tconstraint
  | Solved of 'syntax tconstraint
  | UnifyTerms of crterm * crterm
  | UnifyVars of variable * variable
  | Generalize of int * variable list 

(** [solve tracer c] solves [c] by doing in-place modifications resulting
    in a environment. *)
val solve: ?tracer:('syntax solving_step -> unit) 
  -> 'syntax tconstraint -> 'syntax 

module type SolverException =
sig

  (** [TypingError] is raised when an inconsistency is detected during
      constraint solving. *)
  exception TypingError of position

  (** [UnboundIdentifier] is raised when an identifier is undefined in
      a particular context. *)
  exception UnboundIdentifier of position * PIdentifier.t

  (** [CannotGeneralize] when the type of an expression cannot be
      generalized contrary to what is specified by the programmers
      using type annotations. *)
  exception CannotGeneralize of position * variable

  (** [NonDistinctVariables] is raised when two rigid type variables have
      been unified. *)
  exception NonDistinctVariables of position * (variable list)

end
include SolverException
